00100	VAR: x,y,z,u,v,w;
00200	PRE_PRED: T,C,S,A;
00300	
00400	A1: S(x,y,y,x);
00500	A2: S(u,v,x,y)⊃S(x,y,u,v);
00600	A3: S(u,v,x,y)⊃S(v,u,x,y);
00700	A4: T(x,y,z)⊃T(y,z,x);
00800	A5: T(x,y,z)⊃T(y,x,z);
00900	A6: C(u,v,w,x,y,z)⊃(A(u,v,w,x,y,z)∧A(v,u,w,y,x,z)∧A(u,w,v,x,z,y));
01000	A7: (T(u,v,w)∧T(x,y,z)∧S(u,v,x,y)∧S(v,w,y,z)∧S(u,w,x,z))⊃
01100	            C(u,v,w,x,y,z);
01200	THM:(T(x,y,z)∧S(x,z,y,z))⊃A(z,x,y,z,y,x);;